翻訳と辞書 Words near each other ・ Tyoply ・ Tyoply Stan ・ Tyoply Stan (Moscow Metro) ・ Tyoply Stan District ・ Tyosha River ・ Tyosovo peat narrow gauge railway ・ Tyous Team of Commandos ・ Typ ・ Typaldos D. children's choir ・ Typaldos Lines ・ Typasius ・ Type ・ Type (biology) ・ Type (designation) ・ TYPE (DOS command) ・ Type (model theory) ・ Type (song) ・ Type (Unix) ・ Type 0 ・ Type 0 string theory ・ Type 01 LMAT ・ Type 010 minesweeper ・ Type 0105 gunboat ・ Type 0109 gunboat ・ Type 0112 gunboat ・ Type 02 torpedo boat ・ Type 021-class missile boat ・ Type 022 missile boat ・ Type 024 missile boat ・ Type 025 torpedo boat Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク Type (model theory) ： ウィキペディア英語版 Type (model theory) In model theory and related areas of mathematics, a type is an object that, loosely speaking, describes how a (real or possible) element or elements in a mathematical structure might behave. More precisely, it is a set of first-order formulas in a language ''L'' with free variables ''x''1, ''x''2,…, ''x''''n'' which are true of a sequence of elements of an ''L''-structure $\backslash mathcal$. Depending on the context, types can be complete or partial and they may use a fixed set of constants, ''A'', from the structure $\backslash mathcal$. The question of which types represent actual elements of $\backslash mathcal$ leads to the ideas of saturated models and omitting types. ==Formal definition== Consider a structure $\backslash mathcal$ for a language ''L''. Let ''M'' be the universe of the structure. For every ''A'' ⊆ ''M'', let ''L''(''A'') be the language which is obtained from ''L'' by adding a constant ''c''''a'' for every ''a'' ∈ ''A''. In other words, :$L(A)\; =\; L\; \backslash cup\; \backslash .$ A 1-type (of $\backslash mathcal$) over ''A'' is a set ''p''(''x'') of formulas in ''L''(''A'') with at most one free variable ''x'' (therefore 1-type) such that for every finite subset ''p''0(''x'') ⊆ ''p''(''x'') there is some ''b'' ∈ ''M'', depending on ''p''0(''x''), with $\backslash mathcal\; \backslash models\; p\_0(b)$ (i.e. all formulas in ''p''0(''x'') are true in $\backslash mathcal$ when ''x'' is replaced by ''b''). Similarly an ''n''-type (of $\backslash mathcal$) over ''A'' is defined to be a set ''p''(''x''1,…,''x''''n'') = ''p''(''x'') of formulas in ''L''(''A''), each having its free variables occurring only among the given ''n'' free variables ''x''1,…,''x''''n'', such that for every finite subset ''p''0(''x'') ⊆ ''p''(''x'') there are some elements ''b''1,…,''b''''n'' ∈ ''M'' with $\backslash mathcal\backslash models\; p\_0(b\_1,\backslash ldots,b\_n)$. Complete type refers to those types which are maximal with respect to inclusion, i.e. if ''p''(''x'') is a complete type, then for every $\backslash phi(\backslash boldsymbol)\; \backslash in\; L(A,\backslash boldsymbol)$ either $\backslash phi(\backslash boldsymbol)\; \backslash in\; p(\backslash boldsymbol)$ or $\backslash lnot\backslash phi(\backslash boldsymbol)\; \backslash in\; p(\backslash boldsymbol)$. Any non-complete type is called a partial type. So, the word type in general refers to any ''n''-type, partial or complete, over any chosen set of parameters (possibly the empty set). An ''n''-type ''p''(''x'') is said to be realized in $\backslash mathcal$ if there is an element ''b'' ∈ ''M''''n'' such that $\backslash mathcal\backslash models\; p(\backslash boldsymbol)$. The existence of such a realization is guaranteed for any type by the Compactness theorem, although the realization might take place in some elementary extension of $\backslash mathcal$, rather than in $\backslash mathcal$ itself. If a complete type is realized by ''b'' in $\backslash mathcal$, then the type is typically denoted $tp\_n^/A)$ and referred to as the complete type of ''b'' over ''A''. A type ''p''(''x'') is said to be isolated by ''φ'' if there is a formula ''φ''(''x'') with the property that $\backslash forall\; \backslash psi(\backslash boldsymbol)\; \backslash in\; p(\backslash boldsymbol),\; \backslash varphi(\backslash boldsymbol)\; \backslash rightarrow\; \backslash psi(\backslash boldsymbol)$. Since finite subsets of a type are always realized in $\backslash mathcal$, there is always an element ''b'' ∈ ''M''''n'' such that ''φ''(''b'') is true in $\backslash mathcal$; i.e. $\backslash mathcal\; \backslash models\; \backslash varphi(\backslash boldsymbol)$, thus ''b'' realizes the entire isolated type. So isolated types will be realized in every elementary substructure or extension. Because of this, isolated types can never be omitted (see below). A model that realizes the maximum possible variety of types is called a saturated model, and the ultrapower construction provides one way of producing saturated models. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Type (model theory)」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.